i z j == j <z i 

latex

Up	bool 1, bool 1
Wellformedness Lemmas	le int wf, le int wf
Definitions	b, i <z j
FDL editor aliases	le_int